Iof proof for Lemma inv image ind tp:
1. T : Type
2. r : T
T
3. S : Type
4. f : S
T
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7.
j:S. (k:S. r(f(k),f(j)) 
P(k)) P(j)
8. n : S
9.
x:T, n:S. (f(n) = x) P(n)
P(n)
by (\p.let y = get_var_arg `n` p
bin let r = get_term_arg `f` p
bin
b((((((DTerm (
mk_apply_term r (mvt y)) (-1))
CollapseTHENM (((DTerm (mvt y) (-1))
CollapseTHENA (Declaration
C))
)))
CollapseTHENM (D (-1))))
CollapseTHENM (Hypothesis)) p)
C1: .....wf..... NILNIL
C1: 8. n : S
C1: f(n) 
T
C2: .....antecedent..... NILNIL
C2: 8. n : S
C2: f(n) = f(n)
C.